Nuprl Lemma : ds_property
0,22
postcript
pdf
A
:Type,
d
:DS(
A
),
a
:
A
,
x
,
y
:dstype(
A
;
d
;
a
). {
x
=
y
x
=
y
}
latex
Definitions
dstype(
TypeNames
;
d
;
a
)
,
2of(
t
)
,
{
T
}
,
DS(
A
)
,
x
=
y
,
dseq(
d
;
a
)
,
x
:
A
.
B
(
x
)
,
EqDecider(
T
)
,
t
T
Lemmas
dstype
wf
,
deq
property
,
discrete
struct
wf
origin
A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). {x = y 
x = y} A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). {x = y x = y} x:A. B(x)
T